type t a = K : t (a)
type u a = L : u (a) 
